|
|
Next Generation of Rank-Based Algorithms for Omega Automata
Šmahlíková, Barbora ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
Komplementace Büchiho automatů je klíčovou operací pro terminační analýzu programů, model checking nebo rozhodovací procedury pro různé logiky. Tato práce se zabývá především optimalizacemi rank-based komplementace Büchiho automatů. Původní rank-based algoritmus je sice asymptoticky optimální, přesto může generovat nezbytně velký stavový prostor. Pro praktické použití je tedy žádoucí maximálně redukovat počet vygenerovaných stavů v komplementu. V této práci představíme několik technik pro efektivní komplementaci některých speciálních typů Büchiho automatů, často se vyskytujících v praxi, které jsou založené na jejich struktuře. Některé z navržených technik lze do určité míry rozšířit i pro obecné Büchiho automaty. Techniky představené v této práci byly implementovány jako rozšíření nástroje Ranker pro komplementaci Büchiho automatů. Tyto optimalizace výrazně redukují generovaný stavový prostor a Ranker ve většině případů produkuje menší komplement než ostatní existující nástroje pro komplementaci.
|
|
|
Efficient Automata Techniques and Their Applications
Havlena, Vojtěch ; Jančar, Petr (referee) ; Mayr, Richard (referee) ; Esparza, Javier (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá vývojem efektivních technik pro konečné automaty a jejich aplikace. Zejména se věnujeme konečným automatům použitých pří detekci útoků v síťovém provozu a automatům v rozhodovacích procedurách a verifikaci. V první části práce navrhujeme techniky přibližné redukce nedeterministických automatů, které snižují spotřebu zdrojů v hardwarově akcelerovaném zkoumání obsahu paketů. Druhá část práce je je věnována automatům v rozhodovacích procedurách, zejména slabé monadické logice druhého řádů k následníků (WSkS) a teorie nad řetězci. Navrhujeme novou rozhodovací proceduru pro WS2S založenou na automatových termech, umožňující efektivně prořezávat stavový prostor. Dále studujeme techniky předzpracování WSkS formulí za účelem snížení velikosti konstruovaných automatů. Automaty jsme také aplikovali v rozhodovací proceduře teorie nad řetězci pro efektivní reprezentaci důkazového stromu. V poslední části práce potom navrhujeme optimalizace rank-based komplementace Buchiho automatů, které snižuje počet generovaných stavů během konstrukce komplementu.
|
|
|
Next Generation of Rank-Based Algorithms for Omega Automata
Šmahlíková, Barbora ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
Komplementace Büchiho automatů je klíčovou operací pro terminační analýzu programů, model checking nebo rozhodovací procedury pro různé logiky. Tato práce se zabývá především optimalizacemi rank-based komplementace Büchiho automatů. Původní rank-based algoritmus je sice asymptoticky optimální, přesto může generovat nezbytně velký stavový prostor. Pro praktické použití je tedy žádoucí maximálně redukovat počet vygenerovaných stavů v komplementu. V této práci představíme několik technik pro efektivní komplementaci některých speciálních typů Büchiho automatů, často se vyskytujících v praxi, které jsou založené na jejich struktuře. Některé z navržených technik lze do určité míry rozšířit i pro obecné Büchiho automaty. Techniky představené v této práci byly implementovány jako rozšíření nástroje Ranker pro komplementaci Büchiho automatů. Tyto optimalizace výrazně redukují generovaný stavový prostor a Ranker ve většině případů produkuje menší komplement než ostatní existující nástroje pro komplementaci.
|
|
|
Efficient Automata Techniques and Their Applications
Havlena, Vojtěch ; Jančar, Petr (referee) ; Mayr, Richard (referee) ; Esparza, Javier (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá vývojem efektivních technik pro konečné automaty a jejich aplikace. Zejména se věnujeme konečným automatům použitých pří detekci útoků v síťovém provozu a automatům v rozhodovacích procedurách a verifikaci. V první části práce navrhujeme techniky přibližné redukce nedeterministických automatů, které snižují spotřebu zdrojů v hardwarově akcelerovaném zkoumání obsahu paketů. Druhá část práce je je věnována automatům v rozhodovacích procedurách, zejména slabé monadické logice druhého řádů k následníků (WSkS) a teorie nad řetězci. Navrhujeme novou rozhodovací proceduru pro WS2S založenou na automatových termech, umožňující efektivně prořezávat stavový prostor. Dále studujeme techniky předzpracování WSkS formulí za účelem snížení velikosti konstruovaných automatů. Automaty jsme také aplikovali v rozhodovací proceduře teorie nad řetězci pro efektivní reprezentaci důkazového stromu. V poslední části práce potom navrhujeme optimalizace rank-based komplementace Buchiho automatů, které snižuje počet generovaných stavů během konstrukce komplementu.
|
guest ::
